Nuprl Lemma : Rall-nil
0,22
postcript
pdf
R
:Top.
x
nil.
R
(
x
) ~
latex
Definitions
Top
,
t
T
,
x
:
A
.
B
(
x
)
,
(
L
)
,
x
L
.
R
(
x
)
Lemmas
top
wf
origin
R:Top. 
x
nil.R(x) ~ 
R:Top. xnil.R(x) ~ Tx:A. B(x)(L)xL.R(x)